package main

import (
	"bufio"
	"fmt"
	"os"
	"strconv"
	"strings"
	"time"
)

// ANSI color codes
const (
	colorReset   = "\033[0m"
	colorRed     = "\033[31m"
	colorGreen   = "\033[32m"
	colorYellow  = "\033[33m"
	colorBlue    = "\033[34m"
	colorMagenta = "\033[35m"
	colorCyan    = "\033[36m"
	colorBold    = "\033[1m"
)

func printClause(color string, prefix string, clause []int) {
	fmt.Print(color + "c " + prefix + ": ")
	for _, lit := range clause {
		fmt.Printf("%4d ", lit)
	}
	fmt.Println(colorReset)
}

func parse(filename string) ([][]int, int, bool) {
	file, err := os.Open(filename)
	if err != nil {
		fmt.Println("Error opening file:", err)
		return nil, 0, false
	}
	defer file.Close()

	scanner := bufio.NewScanner(file)
	var buffer []int
	var clauseDB [][]int
	var vars int

	for scanner.Scan() {
		line := scanner.Text()
		line = strings.TrimSpace(line)

		if strings.HasPrefix(line, "c") || strings.HasPrefix(line, "%") {
			continue
		}

		if strings.HasPrefix(line, "p cnf") {
			parts := strings.Fields(line)
			if len(parts) != 4 {
				fmt.Println("Invalid p cnf line:", line)
				return nil, 0, false
			}
			vars, _ = strconv.Atoi(parts[2])
			continue
		}

		terms := strings.Fields(line)
		for _, term := range terms {
			literal, _ := strconv.Atoi(term)
			if literal == 0 {
				if len(buffer) == 0 {
					return nil, 0, false
				}
				clauseDB = append(clauseDB, buffer)
				buffer = make([]int, 0)
			} else {
				buffer = append(buffer, literal)
			}
		}
	}

	if err := scanner.Err(); err != nil {
		fmt.Println("Error reading file:", err)
		return nil, 0, false
	}

	return clauseDB, vars, true
}

func abs(x int) int {
	bit := x >> 31
	return (x ^ bit) - bit
}

func sign(x int) int {
	bit := x >> 31
	return int(1 | bit)
}

func depielle(clauses [][]int, numVars int) bool {

	// Initialize the value array from the pro
	pro := []int{}
	val := make([]int, numVars+1)

nextLit:
	for {

	nextClause:
		for _, clause := range clauses {

			// If clause is longer than the pro, it is always undetermined
			// no need to check each literals further
			if len(clause) > len(pro) {
				continue
			}

			// Check each literal
			uni := 0
			for _, lit := range clause {
				switch val[abs(lit)] {
				// If the literal is true, then the clause is true, no need to check further
				case sign(lit), sign(lit) * 2:
					continue nextClause
				// Be aware of the unassigned literal. If one is found, we check if there's
				// remaining one. Until all remaining literals are assigned false, we get a unit
				// clause.
				case 0:
					if uni == 0 {
						uni = lit
					} else {
						continue nextClause
					}
				default:
				}
			}

			// If we reach here and not because of unit clause, we encounter a conflict.
			if uni == 0 {
				// printClause(colorRed, "CONF", pro)
				for len(pro) > 0 {
					lasLit := pro[len(pro)-1]
					lasAbs := abs(lasLit)

					if val[lasAbs]%2 == 0 {
						val[lasAbs] = 0
						pro = pro[:len(pro)-1]
					} else {
						// printClause(colorYellow, "BACK", pro)
						val[lasAbs] = -val[lasAbs] * 2
						pro[len(pro)-1] = -lasLit
						continue nextLit
					}
				}
				return false
			} else {
				pro = append(pro, uni)
				val[abs(uni)] = sign(uni) * 2
				continue nextLit
			}
		}

		// Reaching here means neither unit clause nor conflict is found.
		for v := 1; v <= numVars; v++ {
			if val[v] == 0 {
				val[v] = 1
				pro = append(pro, v)
				continue nextLit
			}
		}

		fmt.Print(colorGreen + "v ")
		for v := 1; v <= numVars; v++ {
			if val[v]%2 == 0 {
				val[v] = val[v] >> 1
			}
			fmt.Printf("%4d ", v*val[v])
			if v%10 == 0 {
				fmt.Printf("\n  ")
			}
		}
		fmt.Println(colorReset)
		return true
	}
}

func main() {
	startTime := time.Now()

	if len(os.Args) < 2 {
		fmt.Println(colorRed + "Usage: satasm <cnf_file>" + colorReset)
		os.Exit(1)
	}

	clauseTable, vars, parsed := parse(os.Args[1])
	if !parsed {
		fmt.Println(colorRed + colorBold + "s UNSATISFIABLE" + colorReset)
		return
	}

	solved := depielle(clauseTable, vars)
	if solved {
		fmt.Println(colorGreen + colorBold + "s SATISFIABLE" + colorReset)
	} else {
		fmt.Println(colorRed + colorBold + "s UNSATISFIABLE" + colorReset)
	}

	elapsedTime := time.Since(startTime)
	fmt.Printf(colorMagenta+"Total execution time: %s\n"+colorReset, elapsedTime)
}
